$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$), $L$, ${\it L'}$:($T$ List). \\[0ex]($\forall$$x$$\in$$L$. $P$($x$)) $\Rightarrow$ ($L$ = ${\it L'}$) $\Rightarrow$ ($L$ = ${\it L'}$ $\in$ (\{$x$:$T$$\mid$ $P$($x$)\} List))